Nuprl Lemma : es-responsive_wf
0,22
postcript
pdf
es
:ES,
l1
,
l2
:IdLnk,
tg1
,
tg2
:Id. es-responsive(
es
;
l1
;
tg1
;
l2
;
tg2
)
Prop
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
isrcv(
e
)
,
b
,
True
,
T
,
P
Q
,
SqStable(
P
)
,
P
&
Q
,
(
e
<loc
e'
)
,
ES
,
IdLnk
,
Id
,
E
,
sender(
e
)
,
Prop
,
x
.
t
(
x
)
,
e
=rcv(
l
,
tg
).
P
(
e
)
,
e
e'
,
e
=rcv(
l
,
tg
).
P
(
e
)
,
es-responsive(
es
;
l1
;
tg1
;
l2
;
tg2
)
Lemmas
existse-rcv
wf
,
es-le
wf
,
alle-rcv
wf
,
es-locl
wf
,
es-sender
wf
,
es-E
wf
,
Id
wf
,
IdLnk
wf
,
event
system
wf
,
sq
stable
from
decidable
,
decidable
assert
,
assert
wf
,
es-isrcv
wf
origin
es:ES, l1, l2:IdLnk, tg1, tg2:Id. es-responsive(es;l1;tg1;l2;tg2) 
Prop es:ES, l1, l2:IdLnk, tg1, tg2:Id. es-responsive(es;l1;tg1;l2;tg2) Prop Tx:A. B(x)
b
T
Q
x. t(x)e=rcv(l,tg). P(e)
e' 
e=rcv(l,tg). P(e)